﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Collections.ObjectModel;
using System.Diagnostics;

namespace OpSatPlan.Encoder
{
    public class MutexEncoder
    {
        private CnfEncoder mEncoder;
        public MutexEncoder(CnfEncoder encoder)
        {
            this.mEncoder = encoder;
        }

        public void Encode(IList<Operator> operators)
        {
            for (int i = 0; i < operators.Count; i++)
            {
                Operator op1 = operators[i];
                for (int j = i; j < operators.Count; j++)
                {
                    Operator op2 = operators[j];
                    this.Encode(op1, op2);
                }
            }
        }

        private void Encode(Operator op1, Operator op2)
        {
            if (op1 == op2)
            {
				if(op1.MayBeMutex(op2))
                	this.EncodeMutexes(op1, op1.Actions.ToList());
            }
            else
            {
                // check for op mutex
                if (!this.EncodeMutex(op1, op2))
                {
					if(op1.MayBeMutex(op2))
                    	this.EncodeMutexes(op1, op1.Actions.ToList(), op2, op2.Actions.ToList());
                }
            }
        }
        private void EncodeMutexes(Operator op, List<Action> acts)
        {
            for (int i = 0; i < acts.Count; i++)
            {
                Action act1 = acts[i];
                for (int j = i + 1; j < acts.Count; j++)
                {
                    Action act2 = acts[j];
					if(act1.IsMutex(act2))
					{
                    	this.EncodeMutex(op, act1, op, act2);
					}
                }
            }
        }
        private void EncodeMutexes(Operator op1, List<Action> acts1, Operator op2, List<Action> acts2)
        {
			for (int i = 0; i < acts1.Count; i++)
            {
                Action act1 = acts1[i];
                for (int j = 0; j < acts2.Count; j++)
                {
                    Action act2 = acts2[j];
					if(act1.IsMutex(act2))
					{
                    	this.EncodeMutex(op1, act1, op2, act2);	
					}
                }
            }
        }
        private void EncodeMutex(Operator op1, Action act1, Operator op2, Action act2)
        {
            bool found = false;
            ClauseTemplate clause;
			clause = new ClauseTemplate(this.mEncoder);
            clause.Add(op1, false);
            foreach (Identifier id in act1.Identifiers)
            {
                clause.Add(id.AtomicFormula, id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1, !id.Value);
            }
            clause.Add(op2, false);
            foreach (Identifier id in act2.Identifiers)
            {
                clause.Add(id.AtomicFormula, id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1, !id.Value);
            }
            this.mEncoder.WriteClauses(clause);
//            foreach (AtomicFormula del in act1.DeleteEffects)
//            {
//				if(act2.ContainsPrecondition(del))
//				{
//					found = true;
//                    clause = new ClauseTemplate(this.mEncoder);
//                    clause.Add(op1, false);
//                    foreach (Identifier id in act1.Identifiers)
//                    {
//                        clause.Add(id.AtomicFormula, id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1, !id.Value);
//                    }
//                    clause.Add(op2, false);
//                    foreach (Identifier id in act2.Identifiers)
//                    {
//                        clause.Add(id.AtomicFormula, id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1, !id.Value);
//                    }
//                    this.mEncoder.WriteClauses(clause);
//                    break;
//				}
//				else if(act2.ContainsAddEffect(del))
//				{
//					found = true;
//                    clause = new ClauseTemplate(this.mEncoder);
//                    clause.Add(op1, false);
//                    foreach (Identifier id in act1.Identifiers)
//                    {
//                        clause.Add(id.AtomicFormula, id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1, !id.Value);
//                    }
//                    clause.Add(op2, false);
//                    foreach (Identifier id in act2.Identifiers)
//                    {
//                        clause.Add(id.AtomicFormula, id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1, !id.Value);
//                    }
//                    this.mEncoder.WriteClauses(clause);
//                    break;
//				}
//            }
//            if (!found)
//            {
//                foreach (AtomicFormula del in act2.DeleteEffects)
//                {
//					if(act1.ContainsPrecondition(del))
//					{
//						found = true;
//                        clause = new ClauseTemplate(this.mEncoder);
//                        clause.Add(op1, false);
//                        foreach (Identifier id in act1.Identifiers)
//                        {
//                            clause.Add(id.AtomicFormula, id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1, !id.Value);
//                        }
//                        clause.Add(op2, false);
//                        foreach (Identifier id in act2.Identifiers)
//                        {
//                            clause.Add(id.AtomicFormula, id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1, !id.Value);
//                        }
//                        this.mEncoder.WriteClauses(clause);
//                        break;
//					}
//					else if(act1.ContainsAddEffect(del))
//					{
//						found = true;
//                        clause = new ClauseTemplate(this.mEncoder);
//                        clause.Add(op1, false);
//                        foreach (Identifier id in act1.Identifiers)
//                        {
//                            clause.Add(id.AtomicFormula, id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1, !id.Value);
//                        }
//                        clause.Add(op2, false);
//                        foreach (Identifier id in act2.Identifiers)
//                        {
//                            clause.Add(id.AtomicFormula, id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1, !id.Value);
//                        }
//                        this.mEncoder.WriteClauses(clause);
//                        break;
//					}
//                }
//            }
        }
        private bool EncodeMutex(Operator op1, Operator op2)
        {
            bool found = false;
            ClauseTemplate clause;
			found = op1.IsMutex(op2);
			if(found)
			{
				clause = new ClauseTemplate(this.mEncoder);
                clause.Add(op1, false);
                clause.Add(op2, false);
                this.mEncoder.WriteClauses(clause);
			}
//			
//            foreach (ReadOnlyCollection<AtomicFormula> dels in op1.DeleteEffects)
//            {
//				if(dels.Count != 1)
//					continue;
//                foreach (ReadOnlyCollection<AtomicFormula> pres in op2.Preconditions)
//                {
//                    if (dels.Count == 1 && pres.Count == 1 && dels[0] == pres[0])
//                    {
//                        found = true;
//                        clause = new ClauseTemplate(this.mEncoder);
//                        clause.Add(op1, false);
//                        clause.Add(op2, false);
//                        this.mEncoder.WriteClauses(clause);
//                        break;
//                    }
//                }
//                if (!found)
//                {
//                    foreach (ReadOnlyCollection<AtomicFormula> pres in op2.AddEffects)
//                    {
//                        if (dels.Count == 1 && pres.Count == 1 && dels[0] == pres[0])
//                        {
//                            found = true;
//                            clause = new ClauseTemplate(this.mEncoder);
//                            clause.Add(op1, false);
//                            clause.Add(op2, false);
//                            this.mEncoder.WriteClauses(clause);
//                            break;
//                        }
//                    }
//                }
//                if (found)
//                    break;
//            }
//            if (!found)
//            {
//                foreach (ReadOnlyCollection<AtomicFormula> dels in op2.DeleteEffects)
//                {
//					if(dels.Count != 1)
//						continue;
//					
//                    foreach (ReadOnlyCollection<AtomicFormula> pres in op1.Preconditions)
//                    {
//                        if (dels.Count == 1 && pres.Count == 1 && dels[0] == pres[0])
//                        {
//                            found = true;
//                            clause = new ClauseTemplate(this.mEncoder);
//                            clause.Add(op1, false);
//                            clause.Add(op2, false);
//                            this.mEncoder.WriteClauses(clause);
//                            break;
//                        }
//                    }
//                    if (!found)
//                    {
//                        foreach (ReadOnlyCollection<AtomicFormula> pres in op1.AddEffects)
//                        {
//                            if (dels.Count == 1 && pres.Count == 1 && dels[0] == pres[0])
//                            {
//                                found = true;
//                                clause = new ClauseTemplate(this.mEncoder);
//                                clause.Add(op1, false);
//                                clause.Add(op2, false);
//                                this.mEncoder.WriteClauses(clause);
//                                break;
//                            }
//                        }
//                    }
//                    if (found)
//                        break;
//                }
//            }
            return found;
        }
    }
}
